x:Id, L:Knd List, t:Type. t  AtomFree(Type;t)  Feasible(only members of L affect x :t) 

latex

Definitions	IdLnk, t  T, Knd, x:AB(x), False, Id, false, IdDeq, x:A. B(x), eqof(d), f(a), p  q, b, (x  l), P  Q, P & Q, x.A(x), nil, car.cdr, <a,b>, State(ds), f(x), x  dom(f), xdom(f). v=f(x)   P(x;v), ma-frame-compat(A;B), mk-ma, , x : v, f(x)?z, Feasible(M), only members of L affect x :t, type List, Type, AtomFree(T;x)
Lemmas	atom-free wf, assert wf, bor wf, eqof wf, id-deq wf, bfalse wf, Id wf, false wf, Knd wf, IdLnk wf